Current modeling and verification approaches for self-adaptive software rarely consider temporal properties. However, in time-critical application domain, the correct operation of self-adaptive software depends on the correctness of self-adaptive logic as well as temporal properties of self-adaptive software dynamic processes. For this end, temporal properties for self-adaptive software were explicitly defined, such as, monitoring period, delay trigger time, deadline of self-adaptive process, self-adaptive adjusting time and self-adaptive steady time. Then, a Timed Automata Network (TAN) based modeling templates for temporal properties of self-adaptive software dynamic processes were constructed. Finally, the temporal properties were formally described with Timed Computation Tree Logic (TCTL), and then were analyzed and verified. Combining with a self-adaptive example, this paper has validated the proposed approach. The results show that the proposed approach can explicitly depict temporal properties of self-adaptive software, and can reduce its formal modeling complexity.

The standard Unified Modeling Language (UML) and general tools for self-adaptive software could not model Software Fuzzy Self-Adaptation (SFSA) directly in the analysis and design phases. A new approach called Fuzzy Case was proposed by extending UML use case for the modeling of SFSA. By combining the conceptual framework of SFSA and applying the UML extending mechanism, new stereotypes and tagged values were introduced and a meta-model for Fuzzy Case was created. Then, the syntax structure was given and the semantics of Fuzzy Case were defined with Object Constraint Language (OCL). The instance validation shows that, compared with the traditional approaches, Fuzzy Case can express structures of SFSA more explicitly, define semantics of SFSA more accurately and model SFSA more conveniently. The proposed approach plays an important role in improving the development efficiency of SFSA.